Nuprl Lemma : stable-implies3
11,40
postcript
pdf
es
:ES,
i
:Id,
P
:(discrete state@
i
).
@
i
stable
state
.
P
(
state
)
e
@
i
.
P
((discrete state when
e
))
e'
e
.
P
((discrete state when
e'
))
latex
Definitions
f
(
a
)
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
B
(
x
)
,
A
c
B
,
left
+
right
,
P
Q
,
x
:
A
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
,
True
,
T
,
ES
,
Id
,
discrete state@
i
,
(discrete state when
e
)
,
E
,
e
loc
e'
,
,
(
e
<loc
e'
)
,
x
.
A
(
x
)
,
{
T
}
,
x
.
t
(
x
)
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
loc(
e
)
,
s
=
t
,
@
i
stable
state
.
P
(
state
)
,
Type
,
e
@
i
.
P
(
e
)
,
e'
e
.
P
(
e'
)
,
pred(
e
)
,
P
Q
,
SQType(
T
)
,
s
~
t
,
Atom$n
,
(discrete state after
e
)
,
<
a
,
b
>
,
False
,
A
,
t
.1
,
b
,
Void
,
x
,
y
.
t
(
x
;
y
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
{
x
:
A
|
B
(
x
)}
Lemmas
es-loc-pred
,
all
functionality
wrt
iff
,
implies
functionality
wrt
iff
,
wellfounded
functionality
wrt
iff
,
es-locl-iff
,
Id
sq
,
dstate-after-pred
,
es-pred
wf
,
es-pred-locl
,
es-stable
wf
,
es-loc
wf
,
es-locl-wellfnd
,
es-locl
wf
,
es-le
wf
,
es-E
wf
,
es-le-loc
,
es-dstate-when
wf
,
es-dstate
wf
,
squash
wf
,
true
wf
,
Id
wf
,
event
system
wf
,
es-le-iff
origin
es:ES, i:Id, P:(discrete state@i
).
e@i. P((discrete state when e)) e'
e.P((discrete state when e')) es:ES, i:Id, P:(discrete state@i).
e@i. P((discrete state when e)) e'e.P((discrete state when e')) 
T
B(x)
B
Q
T
loc e' 
x.A(x)
x. t(x)
A
b